the_w:World, l:IdLnk, mss:Msg List. withlnk(l;mss)  (t:Idthe_w.M(l,t)) List 

latex

Definitions	P  Q, P & Q, P  Q, World, Msg, withlnk(l;mss), w.M, mapfilter(f;P;L), a = b, mlnk(m), b, 2of(t), Id, , Msg(M), x:A. B(x), t  T, IdLnk
Lemmas	IdLnk wf, Msg wf, assert wf, Id wf, mlnk wf, eq lnk wf, mapfilter wf, world wf, assert-eq-lnk